T:Type, L:(T List). ((null(L)))  (L ~ (firstn(||L|| - 1;L) @ [last(L)])) 

latex

Definitions

Type, t  T, s = t, type List, Void, x:A.B(x), Top, x:AB(x), x:A. B(x), S  T, null(as), b, A, s ~ t, P  Q, #$n, ||as||, i > j, a < b, i <z j, x:A  B(x), P & Q, P  Q, P  Q, (x  l), , A  B, , , False, {x:A| B(x)} , -n, n+m, x before y  l, {i..j}, upto(n), |g|, , Unit, left + right, if a<b then c else d, , True, T, [], a < b, f(a), x f y, a < b, [d], b, p  q, p  q, p q, (i = j), x =a y, n - m, nth_tl(n;as), last(L), [car / cdr], {i...j}, l[i], tl(l), i  j , hd(l), i  j < k

Lemmas

append firstn lastn sq, non neg length, iff wf, rev implies wf, length nth tl, int iseg wf, list decomp, nth tl wf, not functionality wrt iff, assert of null, nat plus properties, nat plus wf, length wf1, mul cancel in lt, add cancel in lt, lt int eq true elim, unit wf, bool wf, before-upto, l before wf, int seg wf, add mono wrt lt, minus mono wrt lt, lt transitivity 2, lt transitivity 1, member upto, length wf nat, le wf, nat wf, l member wf, assert of lt int, non nil length, not wf, assert wf, null wf3, member wf, top wf